* Step 1: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,i/2} / {a/0,b/0,h/1,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g,i} and constructors {a,b,h,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(s(x)) -> c_1(f#(h(s(x)))) g#(x,x) -> c_2(g#(a(),b())) i#(x,x) -> c_3(i#(a(),b())) Weak DPs and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: f#(s(x)) -> c_1(f#(h(s(x)))) g#(x,x) -> c_2(g#(a(),b())) i#(x,x) -> c_3(i#(a(),b())) - Weak TRS: f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,i/2,f#/1,g#/2,i#/2} / {a/0,b/0,h/1,s/1,c_1/1,c_2/1,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,i#} and constructors {a,b,h,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: f#(s(x)) -> c_1(f#(h(s(x)))) g#(x,x) -> c_2(g#(a(),b())) i#(x,x) -> c_3(i#(a(),b())) * Step 3: Trivial WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: f#(s(x)) -> c_1(f#(h(s(x)))) g#(x,x) -> c_2(g#(a(),b())) i#(x,x) -> c_3(i#(a(),b())) - Signature: {f/1,g/2,i/2,f#/1,g#/2,i#/2} / {a/0,b/0,h/1,s/1,c_1/1,c_2/1,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,i#} and constructors {a,b,h,s} + Applied Processor: Trivial + Details: Consider the dependency graph 1:S:f#(s(x)) -> c_1(f#(h(s(x)))) 2:S:g#(x,x) -> c_2(g#(a(),b())) 3:S:i#(x,x) -> c_3(i#(a(),b())) The dependency graph contains no loops, we remove all dependency pairs. * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {f/1,g/2,i/2,f#/1,g#/2,i#/2} / {a/0,b/0,h/1,s/1,c_1/1,c_2/1,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,i#} and constructors {a,b,h,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))